Left Termination of the query pattern e_in_2(g, a) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

e(L, T) :- t(L, T).
e(L, T) :- ','(t(L, .(plus, C)), e(C, T)).
t(L, T) :- n(L, T).
t(L, T) :- ','(n(L, .(star, C)), t(C, T)).
n(.(L, T), T) :- z(L).
n(.(lbrace, A), B) :- e(A, .(rbrace, B)).
z(a).
z(b).
z(c).

Queries:

e(g,a).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

e_in(L, T) → U2(L, T, t_in(L, .(plus, C)))
t_in(L, T) → U5(L, T, n_in(L, .(star, C)))
n_in(.(lbrace, A), B) → U8(A, B, e_in(A, .(rbrace, B)))
e_in(L, T) → U1(L, T, t_in(L, T))
t_in(L, T) → U4(L, T, n_in(L, T))
n_in(.(L, T), T) → U7(L, T, z_in(L))
z_in(c) → z_out(c)
z_in(b) → z_out(b)
z_in(a) → z_out(a)
U7(L, T, z_out(L)) → n_out(.(L, T), T)
U4(L, T, n_out(L, T)) → t_out(L, T)
U1(L, T, t_out(L, T)) → e_out(L, T)
U8(A, B, e_out(A, .(rbrace, B))) → n_out(.(lbrace, A), B)
U5(L, T, n_out(L, .(star, C))) → U6(L, T, t_in(C, T))
U6(L, T, t_out(C, T)) → t_out(L, T)
U2(L, T, t_out(L, .(plus, C))) → U3(L, T, e_in(C, T))
U3(L, T, e_out(C, T)) → e_out(L, T)

The argument filtering Pi contains the following mapping:
e_in(x1, x2)  =  e_in(x1)
U2(x1, x2, x3)  =  U2(x3)
t_in(x1, x2)  =  t_in(x1)
.(x1, x2)  =  .(x1, x2)
plus  =  plus
U5(x1, x2, x3)  =  U5(x3)
n_in(x1, x2)  =  n_in(x1)
star  =  star
lbrace  =  lbrace
U8(x1, x2, x3)  =  U8(x3)
rbrace  =  rbrace
U1(x1, x2, x3)  =  U1(x3)
U4(x1, x2, x3)  =  U4(x3)
U7(x1, x2, x3)  =  U7(x2, x3)
z_in(x1)  =  z_in(x1)
c  =  c
z_out(x1)  =  z_out
b  =  b
a  =  a
n_out(x1, x2)  =  n_out(x2)
t_out(x1, x2)  =  t_out(x2)
e_out(x1, x2)  =  e_out(x2)
U6(x1, x2, x3)  =  U6(x3)
U3(x1, x2, x3)  =  U3(x3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

e_in(L, T) → U2(L, T, t_in(L, .(plus, C)))
t_in(L, T) → U5(L, T, n_in(L, .(star, C)))
n_in(.(lbrace, A), B) → U8(A, B, e_in(A, .(rbrace, B)))
e_in(L, T) → U1(L, T, t_in(L, T))
t_in(L, T) → U4(L, T, n_in(L, T))
n_in(.(L, T), T) → U7(L, T, z_in(L))
z_in(c) → z_out(c)
z_in(b) → z_out(b)
z_in(a) → z_out(a)
U7(L, T, z_out(L)) → n_out(.(L, T), T)
U4(L, T, n_out(L, T)) → t_out(L, T)
U1(L, T, t_out(L, T)) → e_out(L, T)
U8(A, B, e_out(A, .(rbrace, B))) → n_out(.(lbrace, A), B)
U5(L, T, n_out(L, .(star, C))) → U6(L, T, t_in(C, T))
U6(L, T, t_out(C, T)) → t_out(L, T)
U2(L, T, t_out(L, .(plus, C))) → U3(L, T, e_in(C, T))
U3(L, T, e_out(C, T)) → e_out(L, T)

The argument filtering Pi contains the following mapping:
e_in(x1, x2)  =  e_in(x1)
U2(x1, x2, x3)  =  U2(x3)
t_in(x1, x2)  =  t_in(x1)
.(x1, x2)  =  .(x1, x2)
plus  =  plus
U5(x1, x2, x3)  =  U5(x3)
n_in(x1, x2)  =  n_in(x1)
star  =  star
lbrace  =  lbrace
U8(x1, x2, x3)  =  U8(x3)
rbrace  =  rbrace
U1(x1, x2, x3)  =  U1(x3)
U4(x1, x2, x3)  =  U4(x3)
U7(x1, x2, x3)  =  U7(x2, x3)
z_in(x1)  =  z_in(x1)
c  =  c
z_out(x1)  =  z_out
b  =  b
a  =  a
n_out(x1, x2)  =  n_out(x2)
t_out(x1, x2)  =  t_out(x2)
e_out(x1, x2)  =  e_out(x2)
U6(x1, x2, x3)  =  U6(x3)
U3(x1, x2, x3)  =  U3(x3)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

E_IN(L, T) → U21(L, T, t_in(L, .(plus, C)))
E_IN(L, T) → T_IN(L, .(plus, C))
T_IN(L, T) → U51(L, T, n_in(L, .(star, C)))
T_IN(L, T) → N_IN(L, .(star, C))
N_IN(.(lbrace, A), B) → U81(A, B, e_in(A, .(rbrace, B)))
N_IN(.(lbrace, A), B) → E_IN(A, .(rbrace, B))
E_IN(L, T) → U11(L, T, t_in(L, T))
E_IN(L, T) → T_IN(L, T)
T_IN(L, T) → U41(L, T, n_in(L, T))
T_IN(L, T) → N_IN(L, T)
N_IN(.(L, T), T) → U71(L, T, z_in(L))
N_IN(.(L, T), T) → Z_IN(L)
U51(L, T, n_out(L, .(star, C))) → U61(L, T, t_in(C, T))
U51(L, T, n_out(L, .(star, C))) → T_IN(C, T)
U21(L, T, t_out(L, .(plus, C))) → U31(L, T, e_in(C, T))
U21(L, T, t_out(L, .(plus, C))) → E_IN(C, T)

The TRS R consists of the following rules:

e_in(L, T) → U2(L, T, t_in(L, .(plus, C)))
t_in(L, T) → U5(L, T, n_in(L, .(star, C)))
n_in(.(lbrace, A), B) → U8(A, B, e_in(A, .(rbrace, B)))
e_in(L, T) → U1(L, T, t_in(L, T))
t_in(L, T) → U4(L, T, n_in(L, T))
n_in(.(L, T), T) → U7(L, T, z_in(L))
z_in(c) → z_out(c)
z_in(b) → z_out(b)
z_in(a) → z_out(a)
U7(L, T, z_out(L)) → n_out(.(L, T), T)
U4(L, T, n_out(L, T)) → t_out(L, T)
U1(L, T, t_out(L, T)) → e_out(L, T)
U8(A, B, e_out(A, .(rbrace, B))) → n_out(.(lbrace, A), B)
U5(L, T, n_out(L, .(star, C))) → U6(L, T, t_in(C, T))
U6(L, T, t_out(C, T)) → t_out(L, T)
U2(L, T, t_out(L, .(plus, C))) → U3(L, T, e_in(C, T))
U3(L, T, e_out(C, T)) → e_out(L, T)

The argument filtering Pi contains the following mapping:
e_in(x1, x2)  =  e_in(x1)
U2(x1, x2, x3)  =  U2(x3)
t_in(x1, x2)  =  t_in(x1)
.(x1, x2)  =  .(x1, x2)
plus  =  plus
U5(x1, x2, x3)  =  U5(x3)
n_in(x1, x2)  =  n_in(x1)
star  =  star
lbrace  =  lbrace
U8(x1, x2, x3)  =  U8(x3)
rbrace  =  rbrace
U1(x1, x2, x3)  =  U1(x3)
U4(x1, x2, x3)  =  U4(x3)
U7(x1, x2, x3)  =  U7(x2, x3)
z_in(x1)  =  z_in(x1)
c  =  c
z_out(x1)  =  z_out
b  =  b
a  =  a
n_out(x1, x2)  =  n_out(x2)
t_out(x1, x2)  =  t_out(x2)
e_out(x1, x2)  =  e_out(x2)
U6(x1, x2, x3)  =  U6(x3)
U3(x1, x2, x3)  =  U3(x3)
N_IN(x1, x2)  =  N_IN(x1)
U61(x1, x2, x3)  =  U61(x3)
U71(x1, x2, x3)  =  U71(x2, x3)
U51(x1, x2, x3)  =  U51(x3)
U31(x1, x2, x3)  =  U31(x3)
U41(x1, x2, x3)  =  U41(x3)
T_IN(x1, x2)  =  T_IN(x1)
U81(x1, x2, x3)  =  U81(x3)
E_IN(x1, x2)  =  E_IN(x1)
U21(x1, x2, x3)  =  U21(x3)
U11(x1, x2, x3)  =  U11(x3)
Z_IN(x1)  =  Z_IN(x1)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

E_IN(L, T) → U21(L, T, t_in(L, .(plus, C)))
E_IN(L, T) → T_IN(L, .(plus, C))
T_IN(L, T) → U51(L, T, n_in(L, .(star, C)))
T_IN(L, T) → N_IN(L, .(star, C))
N_IN(.(lbrace, A), B) → U81(A, B, e_in(A, .(rbrace, B)))
N_IN(.(lbrace, A), B) → E_IN(A, .(rbrace, B))
E_IN(L, T) → U11(L, T, t_in(L, T))
E_IN(L, T) → T_IN(L, T)
T_IN(L, T) → U41(L, T, n_in(L, T))
T_IN(L, T) → N_IN(L, T)
N_IN(.(L, T), T) → U71(L, T, z_in(L))
N_IN(.(L, T), T) → Z_IN(L)
U51(L, T, n_out(L, .(star, C))) → U61(L, T, t_in(C, T))
U51(L, T, n_out(L, .(star, C))) → T_IN(C, T)
U21(L, T, t_out(L, .(plus, C))) → U31(L, T, e_in(C, T))
U21(L, T, t_out(L, .(plus, C))) → E_IN(C, T)

The TRS R consists of the following rules:

e_in(L, T) → U2(L, T, t_in(L, .(plus, C)))
t_in(L, T) → U5(L, T, n_in(L, .(star, C)))
n_in(.(lbrace, A), B) → U8(A, B, e_in(A, .(rbrace, B)))
e_in(L, T) → U1(L, T, t_in(L, T))
t_in(L, T) → U4(L, T, n_in(L, T))
n_in(.(L, T), T) → U7(L, T, z_in(L))
z_in(c) → z_out(c)
z_in(b) → z_out(b)
z_in(a) → z_out(a)
U7(L, T, z_out(L)) → n_out(.(L, T), T)
U4(L, T, n_out(L, T)) → t_out(L, T)
U1(L, T, t_out(L, T)) → e_out(L, T)
U8(A, B, e_out(A, .(rbrace, B))) → n_out(.(lbrace, A), B)
U5(L, T, n_out(L, .(star, C))) → U6(L, T, t_in(C, T))
U6(L, T, t_out(C, T)) → t_out(L, T)
U2(L, T, t_out(L, .(plus, C))) → U3(L, T, e_in(C, T))
U3(L, T, e_out(C, T)) → e_out(L, T)

The argument filtering Pi contains the following mapping:
e_in(x1, x2)  =  e_in(x1)
U2(x1, x2, x3)  =  U2(x3)
t_in(x1, x2)  =  t_in(x1)
.(x1, x2)  =  .(x1, x2)
plus  =  plus
U5(x1, x2, x3)  =  U5(x3)
n_in(x1, x2)  =  n_in(x1)
star  =  star
lbrace  =  lbrace
U8(x1, x2, x3)  =  U8(x3)
rbrace  =  rbrace
U1(x1, x2, x3)  =  U1(x3)
U4(x1, x2, x3)  =  U4(x3)
U7(x1, x2, x3)  =  U7(x2, x3)
z_in(x1)  =  z_in(x1)
c  =  c
z_out(x1)  =  z_out
b  =  b
a  =  a
n_out(x1, x2)  =  n_out(x2)
t_out(x1, x2)  =  t_out(x2)
e_out(x1, x2)  =  e_out(x2)
U6(x1, x2, x3)  =  U6(x3)
U3(x1, x2, x3)  =  U3(x3)
N_IN(x1, x2)  =  N_IN(x1)
U61(x1, x2, x3)  =  U61(x3)
U71(x1, x2, x3)  =  U71(x2, x3)
U51(x1, x2, x3)  =  U51(x3)
U31(x1, x2, x3)  =  U31(x3)
U41(x1, x2, x3)  =  U41(x3)
T_IN(x1, x2)  =  T_IN(x1)
U81(x1, x2, x3)  =  U81(x3)
E_IN(x1, x2)  =  E_IN(x1)
U21(x1, x2, x3)  =  U21(x3)
U11(x1, x2, x3)  =  U11(x3)
Z_IN(x1)  =  Z_IN(x1)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 1 SCC with 7 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

U21(L, T, t_out(L, .(plus, C))) → E_IN(C, T)
T_IN(L, T) → N_IN(L, T)
T_IN(L, T) → N_IN(L, .(star, C))
N_IN(.(lbrace, A), B) → E_IN(A, .(rbrace, B))
E_IN(L, T) → T_IN(L, .(plus, C))
E_IN(L, T) → U21(L, T, t_in(L, .(plus, C)))
E_IN(L, T) → T_IN(L, T)
U51(L, T, n_out(L, .(star, C))) → T_IN(C, T)
T_IN(L, T) → U51(L, T, n_in(L, .(star, C)))

The TRS R consists of the following rules:

e_in(L, T) → U2(L, T, t_in(L, .(plus, C)))
t_in(L, T) → U5(L, T, n_in(L, .(star, C)))
n_in(.(lbrace, A), B) → U8(A, B, e_in(A, .(rbrace, B)))
e_in(L, T) → U1(L, T, t_in(L, T))
t_in(L, T) → U4(L, T, n_in(L, T))
n_in(.(L, T), T) → U7(L, T, z_in(L))
z_in(c) → z_out(c)
z_in(b) → z_out(b)
z_in(a) → z_out(a)
U7(L, T, z_out(L)) → n_out(.(L, T), T)
U4(L, T, n_out(L, T)) → t_out(L, T)
U1(L, T, t_out(L, T)) → e_out(L, T)
U8(A, B, e_out(A, .(rbrace, B))) → n_out(.(lbrace, A), B)
U5(L, T, n_out(L, .(star, C))) → U6(L, T, t_in(C, T))
U6(L, T, t_out(C, T)) → t_out(L, T)
U2(L, T, t_out(L, .(plus, C))) → U3(L, T, e_in(C, T))
U3(L, T, e_out(C, T)) → e_out(L, T)

The argument filtering Pi contains the following mapping:
e_in(x1, x2)  =  e_in(x1)
U2(x1, x2, x3)  =  U2(x3)
t_in(x1, x2)  =  t_in(x1)
.(x1, x2)  =  .(x1, x2)
plus  =  plus
U5(x1, x2, x3)  =  U5(x3)
n_in(x1, x2)  =  n_in(x1)
star  =  star
lbrace  =  lbrace
U8(x1, x2, x3)  =  U8(x3)
rbrace  =  rbrace
U1(x1, x2, x3)  =  U1(x3)
U4(x1, x2, x3)  =  U4(x3)
U7(x1, x2, x3)  =  U7(x2, x3)
z_in(x1)  =  z_in(x1)
c  =  c
z_out(x1)  =  z_out
b  =  b
a  =  a
n_out(x1, x2)  =  n_out(x2)
t_out(x1, x2)  =  t_out(x2)
e_out(x1, x2)  =  e_out(x2)
U6(x1, x2, x3)  =  U6(x3)
U3(x1, x2, x3)  =  U3(x3)
N_IN(x1, x2)  =  N_IN(x1)
U51(x1, x2, x3)  =  U51(x3)
T_IN(x1, x2)  =  T_IN(x1)
E_IN(x1, x2)  =  E_IN(x1)
U21(x1, x2, x3)  =  U21(x3)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ UsableRulesReductionPairsProof

Q DP problem:
The TRS P consists of the following rules:

U51(n_out(.(star, C))) → T_IN(C)
T_IN(L) → U51(n_in(L))
N_IN(.(lbrace, A)) → E_IN(A)
T_IN(L) → N_IN(L)
E_IN(L) → U21(t_in(L))
U21(t_out(.(plus, C))) → E_IN(C)
E_IN(L) → T_IN(L)

The TRS R consists of the following rules:

e_in(L) → U2(t_in(L))
t_in(L) → U5(n_in(L))
n_in(.(lbrace, A)) → U8(e_in(A))
e_in(L) → U1(t_in(L))
t_in(L) → U4(n_in(L))
n_in(.(L, T)) → U7(T, z_in(L))
z_in(c) → z_out
z_in(b) → z_out
z_in(a) → z_out
U7(T, z_out) → n_out(T)
U4(n_out(T)) → t_out(T)
U1(t_out(T)) → e_out(T)
U8(e_out(.(rbrace, B))) → n_out(B)
U5(n_out(.(star, C))) → U6(t_in(C))
U6(t_out(T)) → t_out(T)
U2(t_out(.(plus, C))) → U3(e_in(C))
U3(e_out(T)) → e_out(T)

The set Q consists of the following terms:

e_in(x0)
t_in(x0)
n_in(x0)
z_in(x0)
U7(x0, x1)
U4(x0)
U1(x0)
U8(x0)
U5(x0)
U6(x0)
U2(x0)
U3(x0)

We have to consider all (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

U51(n_out(.(star, C))) → T_IN(C)
T_IN(L) → U51(n_in(L))
N_IN(.(lbrace, A)) → E_IN(A)
T_IN(L) → N_IN(L)
E_IN(L) → U21(t_in(L))
U21(t_out(.(plus, C))) → E_IN(C)
The following rules are removed from R:

n_in(.(lbrace, A)) → U8(e_in(A))
n_in(.(L, T)) → U7(T, z_in(L))
z_in(c) → z_out
z_in(b) → z_out
z_in(a) → z_out
U7(T, z_out) → n_out(T)
U8(e_out(.(rbrace, B))) → n_out(B)
U2(t_out(.(plus, C))) → U3(e_in(C))
U3(e_out(T)) → e_out(T)
U5(n_out(.(star, C))) → U6(t_in(C))
U6(t_out(T)) → t_out(T)
Used ordering: POLO with Polynomial interpretation [25]:

POL(.(x1, x2)) = 2·x1 + 2·x2   
POL(E_IN(x1)) = 2 + 2·x1   
POL(N_IN(x1)) = x1   
POL(T_IN(x1)) = 2 + 2·x1   
POL(U1(x1)) = x1   
POL(U2(x1)) = x1   
POL(U21(x1)) = x1   
POL(U3(x1)) = 1 + x1   
POL(U4(x1)) = x1   
POL(U5(x1)) = x1   
POL(U51(x1)) = 1 + x1   
POL(U6(x1)) = 2 + x1   
POL(U7(x1, x2)) = 2·x1 + x2   
POL(U8(x1)) = x1   
POL(a) = 2   
POL(b) = 2   
POL(c) = 1   
POL(e_in(x1)) = 2·x1   
POL(e_out(x1)) = x1   
POL(lbrace) = 1   
POL(n_in(x1)) = 2·x1   
POL(n_out(x1)) = x1   
POL(plus) = 2   
POL(rbrace) = 0   
POL(star) = 2   
POL(t_in(x1)) = 2·x1   
POL(t_out(x1)) = x1   
POL(z_in(x1)) = 2·x1   
POL(z_out) = 2   



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ UsableRulesReductionPairsProof
                    ↳ QDP
                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

E_IN(L) → T_IN(L)

The TRS R consists of the following rules:

t_in(L) → U5(n_in(L))
t_in(L) → U4(n_in(L))
U4(n_out(T)) → t_out(T)
e_in(L) → U2(t_in(L))
e_in(L) → U1(t_in(L))
U1(t_out(T)) → e_out(T)

The set Q consists of the following terms:

e_in(x0)
t_in(x0)
n_in(x0)
z_in(x0)
U7(x0, x1)
U4(x0)
U1(x0)
U8(x0)
U5(x0)
U6(x0)
U2(x0)
U3(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.